$\forall$$P$:(chain\_master()$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$${\it list}$:(Id List). $P$(cmconfig(${\it list}$)))
\\[0ex]$\Rightarrow$ ($\forall$${\it from}$, ${\it to}$:Id, ${\it num}$:$\mathbb{N}$. $P$(cmseq(${\it from}$;${\it to}$;${\it num}$)))
\\[0ex]$\Rightarrow$ \{$\forall$$x$:chain\_master(). $P$($x$)\}